/**
 * This class implements the logic behind the BDD for the n-queens problem
 * You should implement all the missing methods
 * 
 * @author Stavros Amanatidis
 *
 */
import java.util.ArrayList;

import net.sf.javabdd.*;

public class QueensLogic
{
	private int			x	= 0;
	private int			y	= 0;
	private int[][]		board;
	private int			size;
	private int			vars;

	private BDDFactory	fact;
	private BDD			bdd;

	public QueensLogic()
	{
		vars = 0;
		fact = JFactory.init(2000000, 200000);
	}

	public void initializeGame(int size)
	{
		this.size = size;
		this.vars = size * size;

		this.x = size;
		this.y = size;
		this.board = new int[x][y];

		fact.setVarNum(vars);
		buildBDD();
	}

	public int[][] getGameBoard()
	{
		return board;
	}

	public boolean insertQueen(int column, int row)
	{
		if (board[column][row] == -1 || board[column][row] == 1)
		{
			return true;
		}

		board[column][row] = 1;

		updateBDD(column, row);

		return true;
	}

	// Builds the initial BDD based on 5 different rules
	private void buildBDD()
	{
		BDD tmpBDD = null;

		// At least one queen in each row
		for (int row = 0; row < size; row++)
		{
			BDD rowBDD = null;

			for (int col = 0; col < size; col++)
			{
				if (col == 0)
					rowBDD = posToVar(col, row);
				else
					rowBDD = rowBDD.or(posToVar(col, row));
			}

			if (row == 0)
				tmpBDD = rowBDD;
			else
				tmpBDD = tmpBDD.apply(rowBDD, BDDFactory.and);
		}

		bdd = tmpBDD;

		tmpBDD = null;

		// Only one queen in each row
		for (int row = 0; row < size; row++)
		{
			BDD rowBDD = null;

			for (int col = 0; col < size; col++)
			{
				BDD subRowBDD = posToVar(col, row);

				for (int subCol = 0; subCol < size; subCol++)
				{
					if (subCol != col)
						subRowBDD = subRowBDD.and(posToVar(subCol, row).not());
				}

				if (col == 0)
					rowBDD = subRowBDD;
				else
					rowBDD = rowBDD.apply(subRowBDD, BDDFactory.or);
			}

			if (row == 0)
				tmpBDD = rowBDD;
			else
				tmpBDD = tmpBDD.apply(rowBDD, BDDFactory.and);
		}

		bdd = bdd.apply(tmpBDD, BDDFactory.and);

		tmpBDD = null;

		// Only one queen in each column
		for (int col = 0; col < size; col++)
		{
			BDD colBDD = null;

			for (int row = 0; row < size; row++)
			{
				BDD subColBDD = posToVar(col, row);

				for (int subRow = 0; subRow < size; subRow++)
				{
					if (subRow != row)
						subColBDD = subColBDD.and(posToVar(col, subRow).not());
				}

				if (row == 0)
					colBDD = subColBDD;
				else
					colBDD = colBDD.apply(subColBDD, BDDFactory.or);
			}

			if (col == 0)
				tmpBDD = colBDD;
			else
				tmpBDD = tmpBDD.apply(colBDD, BDDFactory.and);
		}

		bdd = bdd.apply(tmpBDD, BDDFactory.and);

		tmpBDD = null;

		// Only one queen in each right-down diagonal
		for (int col = 0; col < size; col++)
		{
			ArrayList<BDD> vars = new ArrayList<BDD>();

			for (int x=col, y=0; x < size && y < size; x++, y++)
				vars.add(posToVar(x, y));

			BDD subBDD = null;

			for (BDD bdd : vars)
			{
				BDD subSubBDD = bdd;

				for (BDD bdd1 : vars)
				{
					if (bdd != bdd1)
						subSubBDD = subSubBDD.and(bdd1.not());
				}

				if (subBDD == null)
					subBDD = subSubBDD;
				else
					subBDD = subBDD.apply(subSubBDD, BDDFactory.or);
			}

			BDD subSubBDD = null;

			for (BDD bdd : vars)
			{
				if (subSubBDD == null)
					subSubBDD = bdd.not();				
				else
					subSubBDD = subSubBDD.and(bdd.not());
			}

			subBDD = subBDD.apply(subSubBDD, BDDFactory.or);

			if (tmpBDD == null)
				tmpBDD = subBDD;
			else
				tmpBDD = tmpBDD.apply(subBDD, BDDFactory.and);
		}

		for (int row = 1; row < size; row++)
		{
			ArrayList<BDD> vars = new ArrayList<BDD>();

			for (int x=0, y=row; x < size && y < size; x++, y++)
				vars.add(posToVar(x, y));

			BDD subBDD = null;

			for (BDD bdd : vars)
			{
				BDD subSubBDD = bdd;

				for (BDD bdd1 : vars)
				{
					if (bdd != bdd1)
						subSubBDD = subSubBDD.and(bdd1.not());
				}

				if (subBDD == null)
					subBDD = subSubBDD;
				else
					subBDD = subBDD.apply(subSubBDD, BDDFactory.or);
			}

			BDD subSubBDD = null;

			for (BDD bdd : vars)
			{
				if (subSubBDD == null)
					subSubBDD = bdd.not();				
				else
					subSubBDD = subSubBDD.and(bdd.not());
			}

			subBDD = subBDD.apply(subSubBDD, BDDFactory.or);

			if (tmpBDD == null)
				tmpBDD = subBDD;
			else
				tmpBDD = tmpBDD.apply(subBDD, BDDFactory.and);
		}

		bdd = bdd.apply(tmpBDD, BDDFactory.and);
		
		tmpBDD = null;

		// Only one queen in each left-down diagonal
		for (int col = 0; col < size; col++)
		{
			ArrayList<BDD> vars = new ArrayList<BDD>();

			for (int x=col, y=0; x >= 0 && y < size; x--, y++)
				vars.add(posToVar(x, y));

			BDD subBDD = null;

			for (BDD bdd : vars)
			{
				BDD subSubBDD = bdd;

				for (BDD bdd1 : vars)
				{
					if (bdd != bdd1)
						subSubBDD = subSubBDD.and(bdd1.not());
				}

				if (subBDD == null)
					subBDD = subSubBDD;
				else
					subBDD = subBDD.apply(subSubBDD, BDDFactory.or);
			}

			BDD subSubBDD = null;

			for (BDD bdd : vars)
			{
				if (subSubBDD == null)
					subSubBDD = bdd.not();				
				else
					subSubBDD = subSubBDD.and(bdd.not());
			}

			subBDD = subBDD.apply(subSubBDD, BDDFactory.or);

			if (tmpBDD == null)
				tmpBDD = subBDD;
			else
				tmpBDD = tmpBDD.apply(subBDD, BDDFactory.and);
		}

		for (int row = 1; row < size; row++)
		{
			ArrayList<BDD> vars = new ArrayList<BDD>();

			for (int x=size-1, y=row; x >= 0 && y < size; x--, y++)
				vars.add(posToVar(x, y));

			BDD subBDD = null;

			for (BDD bdd : vars)
			{
				BDD subSubBDD = bdd;

				for (BDD bdd1 : vars)
				{
					if (bdd != bdd1)
						subSubBDD = subSubBDD.and(bdd1.not());
				}

				if (subBDD == null)
					subBDD = subSubBDD;
				else
					subBDD = subBDD.apply(subSubBDD, BDDFactory.or);
			}

			BDD subSubBDD = null;

			for (BDD bdd : vars)
			{
				if (subSubBDD == null)
					subSubBDD = bdd.not();				
				else
					subSubBDD = subSubBDD.and(bdd.not());
			}

			subBDD = subBDD.apply(subSubBDD, BDDFactory.or);

			if (tmpBDD == null)
				tmpBDD = subBDD;
			else
				tmpBDD = tmpBDD.apply(subBDD, BDDFactory.and);
		}

		bdd = bdd.apply(tmpBDD, BDDFactory.and);
	}

	// Updates the BDD according to a newly inserted queen and restricts the board
	// in order to force a solution to the problem.
	private void updateBDD(int col, int row)
	{
		bdd = bdd.restrict(posToVar(col, row));

		for (int r = 0; r < size; r++)
		{
			for (int c = 0; c < size; c++)
			{
				BDD var = posToVar(c, r);

				if (bdd.restrict(var).isZero())
					board[c][r] = -1;
				else if (bdd.restrict(var.not()).isZero())
					board[c][r] = 1;
			}
		}
	}

	private BDD posToVar(int col, int row)
	{
		return fact.ithVar(row * size + col);
	}
}